/LMAR=0/XLINE=3/FONT#0=BASL30/FONT#1=BASI30/FONT#2=BASB30/FONT#10=BAXM30/FONT#11=ZERO30/FONT#12=GRKL30/FONT#13=SUP/FONT#14=MATH30/FONT#3=STA200/FONT#4=NGB25
␈↓ ↓H␈↓␈↓βS␈↓∧ Artificial Intelligence Laboratory, STANFORD UNIVERSITY, Stanford, California 94305

␈↓ ↓H␈↓∧Telephone 415 497-4430␈↓ 
⊗June 19, 1979 




␈↓ ↓H␈↓Dr. J Strother Moore
␈↓ ↓H␈↓SRI International
␈↓ ↓H␈↓333 Ravenswood Ave.
␈↓ ↓H␈↓Menlo Park CA 94025

␈↓ ↓H␈↓Dear J:

␈↓ ↓H␈↓        Enclosed␈α
is␈αanother␈α
proof␈αof␈α
the␈αcorrectness␈α
of␈α␈↓↓tak␈↓␈α
from␈αA.␈α
Nozaki,␈αwhom␈α
I␈αdon't␈α
remember
␈↓ ↓H␈↓having␈α∪met.␈α∩ I␈α∪have␈α∩read␈α∪the␈α∩proof,␈α∪and␈α∪I␈α∩believe␈α∪it.␈α∩ I␈α∪think␈α∩it␈α∪can␈α∩be␈α∪converted␈α∪into␈α∩a
␈↓ ↓H␈↓lexicographic␈αproof␈αor,␈αas␈αI␈αlike␈αto␈αthink␈αof␈αit,␈αan␈αinduction␈αup␈αto␈α␈↓w␈↓
2␈↓.␈α It␈αcovers␈αthe␈αreal␈αcase␈αalso,
␈↓ ↓H␈↓and␈α⊗its␈α∃inductions␈α⊗are␈α∃unequivocally␈α⊗on␈α∃non-negative␈α⊗integers␈α∃only.␈α⊗ The␈α∃amount␈α⊗of␈α∃real
␈↓ ↓H␈↓arithmetic␈αthat␈αhas␈αto␈αbe␈αaxiomatized␈αto␈αjustify␈αit␈α
seems␈αtrivial.␈α O≥␈αhand␈αit␈αlooks␈αlike␈αwe␈αneed␈α
to
␈↓ ↓H␈↓know␈αthat␈αthe␈αreals␈αare␈αtotally␈αordered,␈αthat␈α␈↓∞i␈↓↓x␈↓∞j␈↓␈αis␈αmonotonic␈αand␈αthat␈αit␈αsatis≡es␈α␈↓∞i␈↓↓x - ␈↓1␈↓∞j␈↓↓ = ␈↓∞i␈↓↓x␈↓∞j␈↓ - 1.
␈↓ ↓H␈↓Richard plans to do the Nozaki proof in FOL.

␈↓ ↓H␈↓        I␈αread␈αyours␈αand␈αbalked␈αat␈αthe␈αpossibility␈αthat␈αsubtractions␈αthat␈αare␈αset␈αto␈αzero␈αrather␈αthan
␈↓ ↓H␈↓being␈α⊂allowed␈α⊂to␈α⊂go␈α⊂negative␈α⊂might␈α⊂a≥ect␈α∂its␈α⊂correctness.␈α⊂ Unfortunately,␈α⊂I␈α⊂don't␈α⊂have␈α⊂time␈α∂to
␈↓ ↓H␈↓reread it and see if I still balk.

␈↓ ↓H␈↓        Enclosed␈α∩is␈α∩an␈α∩␈↓↓Elephant␈↓.␈α∩ I␈α∩suppose␈α∩your␈α∩system␈α∩could␈α∩do␈α∩Elephant␈α∩proofs␈α∩also,␈α∩since
␈↓ ↓H␈↓Elephant␈α∞programs␈α∂are␈α∞also␈α∂just␈α∞sentences␈α∞of␈α∂≡rst␈α∞order␈α∂logic,␈α∞but␈α∞maybe␈α∂the␈α∞heuristics␈α∂are␈α∞too
␈↓ ↓H␈↓di≥erent.  Your reaction would be interesting.


␈↓ ↓H␈↓Best regards,



␈↓ ↓H␈↓John McCarthy
␈↓ ↓H␈↓Director
␈↓ ↓H␈↓Professor of Computer Science